For logic programs with arithmetic predicates, showing termination is noteasy, since the usual order for the integers is not well-founded. A new method,easily incorporated in the TermiLog system for automatic termination analysis,is presented for showing termination in this case. The method consists of the following steps: First, a finite abstract domainfor representing the range of integers is deduced automatically. Based on thisabstraction, abstract interpretation is applied to the program. The result is afinite number of atoms abstracting answers to queries which are used to extendthe technique of query-mapping pairs. For each query-mapping pair that ispotentially non-terminating, a bounded (integer-valued) termination function isguessed. If traversing the pair decreases the value of the terminationfunction, then termination is established. Simple functions often suffice foreach query-mapping pair, and that gives our approach an edge over the classicalapproach of using a single termination function for all loops, which mustinevitably be more complicated and harder to guess automatically. It is worthnoting that the termination of McCarthy's 91 function can be shownautomatically using our method. In summary, the proposed approach is based on combining a finite abstractionof the integers with the technique of the query-mapping pairs, and isessentially capable of dividing a termination proof into several cases, suchthat a simple termination function suffices for each case. Consequently, thewhole process of proving termination can be done automatically in the frameworkof TermiLog and similar systems.
展开▼
